Termination w.r.t. Q of the following Term Rewriting System could be proven:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(s(x), y) → f(x, s(s(x)))
f(x, s(s(y))) → f(y, x)
Q is empty.
↳ QTRS
↳ AAECC Innermost
Q restricted rewrite system:
The TRS R consists of the following rules:
f(s(x), y) → f(x, s(s(x)))
f(x, s(s(y))) → f(y, x)
Q is empty.
We have applied [19,8] to switch to innermost. The TRS R 1 is none
The TRS R 2 is
f(s(x), y) → f(x, s(s(x)))
f(x, s(s(y))) → f(y, x)
The signature Sigma is {f}
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
f(s(x), y) → f(x, s(s(x)))
f(x, s(s(y))) → f(y, x)
The set Q consists of the following terms:
f(s(x0), x1)
f(x0, s(s(x1)))
Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:
F(x, s(s(y))) → F(y, x)
F(s(x), y) → F(x, s(s(x)))
The TRS R consists of the following rules:
f(s(x), y) → f(x, s(s(x)))
f(x, s(s(y))) → f(y, x)
The set Q consists of the following terms:
f(s(x0), x1)
f(x0, s(s(x1)))
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ UsableRulesProof
Q DP problem:
The TRS P consists of the following rules:
F(x, s(s(y))) → F(y, x)
F(s(x), y) → F(x, s(s(x)))
The TRS R consists of the following rules:
f(s(x), y) → f(x, s(s(x)))
f(x, s(s(y))) → f(y, x)
The set Q consists of the following terms:
f(s(x0), x1)
f(x0, s(s(x1)))
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
Q DP problem:
The TRS P consists of the following rules:
F(x, s(s(y))) → F(y, x)
F(s(x), y) → F(x, s(s(x)))
R is empty.
The set Q consists of the following terms:
f(s(x0), x1)
f(x0, s(s(x1)))
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
f(s(x0), x1)
f(x0, s(s(x1)))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ ForwardInstantiation
Q DP problem:
The TRS P consists of the following rules:
F(x, s(s(y))) → F(y, x)
F(s(x), y) → F(x, s(s(x)))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule F(x, s(s(y))) → F(y, x) we obtained the following new rules:
F(x0, s(s(s(y_0)))) → F(s(y_0), x0)
F(s(s(y_1)), s(s(x1))) → F(x1, s(s(y_1)))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
Q DP problem:
The TRS P consists of the following rules:
F(s(x), y) → F(x, s(s(x)))
F(x0, s(s(s(y_0)))) → F(s(y_0), x0)
F(s(s(y_1)), s(s(x1))) → F(x1, s(s(y_1)))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule F(s(x), y) → F(x, s(s(x))) we obtained the following new rules:
F(s(s(s(y_0))), x1) → F(s(s(y_0)), s(s(s(s(y_0)))))
F(s(s(y_0)), x1) → F(s(y_0), s(s(s(y_0))))
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
F(s(s(s(y_0))), x1) → F(s(s(y_0)), s(s(s(s(y_0)))))
F(x0, s(s(s(y_0)))) → F(s(y_0), x0)
F(s(s(y_1)), s(s(x1))) → F(x1, s(s(y_1)))
F(s(s(y_0)), x1) → F(s(y_0), s(s(s(y_0))))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
F(s(s(s(y_0))), x1) → F(s(s(y_0)), s(s(s(s(y_0)))))
F(x0, s(s(s(y_0)))) → F(s(y_0), x0)
F(s(s(y_1)), s(s(x1))) → F(x1, s(s(y_1)))
F(s(s(y_0)), x1) → F(s(y_0), s(s(s(y_0))))
The remaining pairs can at least be oriented weakly.
none
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:
Tuple symbols:
| M( F(x1, x2) ) = | 0 | + | | · | x1 | + | | · | x2 |
Matrix type:
We used a basic matrix type which is not further parametrizeable.
As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:
none
↳ QTRS
↳ AAECC Innermost
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ ForwardInstantiation
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.